(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 32))
(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun x3 () (_ BitVec 32))
(declare-fun x4 () (_ BitVec 32))
(declare-fun x5 () Bool)
(declare-fun x6 () (_ BitVec 32))
(declare-fun x7 () (_ BitVec 32))
(declare-fun x8 () (_ BitVec 32))
(assert (let ((?v_21 (bvadd (bvmul (bvsub (_ bv0 32) (_ bv48 32)) x4) (_ bv0 32)))) (and true x5 true (not (= x1 (_ bv0 32))) true (= ?v_21 x6) (= x6 x7) (= x7 x0) (= x0 x2) (= x2 x8) (= x8 x3) (= x3 x1))))
(check-sat)
(exit)
